Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
ACTIVATE(n__div(X1, X2)) → DIV(activate(X1), X2)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → S(activate(X))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__0, Y) → 01
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__0) → 01
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
ACTIVATE(n__div(X1, X2)) → DIV(activate(X1), X2)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → S(activate(X))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__0, Y) → 01
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__0) → 01
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
Q DP problem:
The TRS P consists of the following rules:
DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
ACTIVATE(n__div(X1, X2)) → DIV(activate(X1), X2)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IF(false, X, Y) → ACTIVATE(Y) we obtained the following new rules:
IF(false, n__s(n__div(n__minus(y_4, y_6), n__s(y_8))), n__0) → ACTIVATE(n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
IF(false, n__s(n__div(n__minus(y_4, y_6), n__s(y_8))), n__0) → ACTIVATE(n__0)
ACTIVATE(n__div(X1, X2)) → DIV(activate(X1), X2)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
ACTIVATE(n__div(X1, X2)) → DIV(activate(X1), X2)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__div(X1, X2)) → DIV(activate(X1), X2) at position [0] we obtained the following new rules:
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
ACTIVATE(n__div(n__0, y1)) → DIV(0, y1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__0, y1)) → DIV(0, y1)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y)) at position [0] we obtained the following new rules:
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
ACTIVATE(n__div(n__0, y1)) → DIV(0, y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule DIV(s(X), n__s(Y)) → GEQ(X, activate(Y)) at position [1] we obtained the following new rules:
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
ACTIVATE(n__div(n__0, y1)) → DIV(0, y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y)) at position [0] we obtained the following new rules:
GEQ(n__s(n__0), n__s(y1)) → GEQ(0, activate(y1))
GEQ(n__s(n__minus(x0, x1)), n__s(y1)) → GEQ(minus(x0, x1), activate(y1))
GEQ(n__s(n__div(x0, x1)), n__s(y1)) → GEQ(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1))
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__0, y1)) → DIV(0, y1)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__div(x0, x1)), n__s(y1)) → GEQ(div(activate(x0), x1), activate(y1))
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
GEQ(n__s(n__0), n__s(y1)) → GEQ(0, activate(y1))
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(x0, x1)), n__s(y1)) → GEQ(minus(x0, x1), activate(y1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__div(n__0, y1)) → DIV(0, y1) at position [0] we obtained the following new rules:
ACTIVATE(n__div(n__0, y0)) → DIV(n__0, y0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(n__0, y0)) → DIV(n__0, y0)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
GEQ(n__s(n__div(x0, x1)), n__s(y1)) → GEQ(div(activate(x0), x1), activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
GEQ(n__s(n__0), n__s(y1)) → GEQ(0, activate(y1))
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(x0, x1)), n__s(y1)) → GEQ(minus(x0, x1), activate(y1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
GEQ(n__s(n__div(x0, x1)), n__s(y1)) → GEQ(div(activate(x0), x1), activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
GEQ(n__s(n__0), n__s(y1)) → GEQ(0, activate(y1))
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(x0, x1)), n__s(y1)) → GEQ(minus(x0, x1), activate(y1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(n__0), n__s(y1)) → GEQ(0, activate(y1)) at position [0] we obtained the following new rules:
GEQ(n__s(n__0), n__s(y0)) → GEQ(n__0, activate(y0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1))
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__0), n__s(y0)) → GEQ(n__0, activate(y0))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__div(x0, x1)), n__s(y1)) → GEQ(div(activate(x0), x1), activate(y1))
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(x0, x1)), n__s(y1)) → GEQ(minus(x0, x1), activate(y1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
GEQ(n__s(n__div(x0, x1)), n__s(y1)) → GEQ(div(activate(x0), x1), activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(x0, x1)), n__s(y1)) → GEQ(minus(x0, x1), activate(y1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(n__minus(x0, x1)), n__s(y1)) → GEQ(minus(x0, x1), activate(y1)) at position [1] we obtained the following new rules:
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), 0)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1))
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__div(x0, x1)), n__s(y1)) → GEQ(div(activate(x0), x1), activate(y1))
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(n__div(x0, x1)), n__s(y1)) → GEQ(div(activate(x0), x1), activate(y1)) at position [1] we obtained the following new rules:
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), 0)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(n__s(x0)), n__s(y1)) → GEQ(s(activate(x0)), activate(y1)) at position [1] we obtained the following new rules:
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), 0)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(x0), n__s(y1)) → GEQ(x0, activate(y1)) at position [1] we obtained the following new rules:
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), 0)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
DIV(s(y0), n__s(n__0)) → GEQ(y0, 0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule DIV(s(y0), n__s(n__0)) → GEQ(y0, 0) at position [1] we obtained the following new rules:
DIV(s(y0), n__s(n__0)) → GEQ(y0, n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), 0)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
DIV(s(y0), n__s(n__0)) → GEQ(y0, n__0)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), 0)
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), 0) at position [1] we obtained the following new rules:
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__0)) → GEQ(minus(y0, y1), n__0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), 0) at position [1] we obtained the following new rules:
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(n__div(y0, y1)), n__s(n__0)) → GEQ(div(activate(y0), y1), n__0)
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), 0) at position [1] we obtained the following new rules:
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
GEQ(n__s(n__s(y0)), n__s(n__0)) → GEQ(s(activate(y0)), n__0)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, 0) at position [1] we obtained the following new rules:
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__0)) → GEQ(y0, n__0)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1))
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(n__div(x0, x1)), n__s(y1)) → MINUS(div(activate(x0), x1), activate(y1)) at position [1] we obtained the following new rules:
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), 0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), 0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(n__minus(x0, x1)), n__s(y1)) → MINUS(minus(x0, x1), activate(y1)) at position [1] we obtained the following new rules:
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0)
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), 0)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1))
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(x0), n__s(y1)) → MINUS(x0, activate(y1)) at position [1] we obtained the following new rules:
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1))
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), 0)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(n__s(x0)), n__s(y1)) → MINUS(s(activate(x0)), activate(y1)) at position [1] we obtained the following new rules:
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), 0)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(n__0), n__s(y1)) → MINUS(0, activate(y1)) at position [0] we obtained the following new rules:
MINUS(n__s(n__0), n__s(y0)) → MINUS(n__0, activate(y0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
MINUS(n__s(n__0), n__s(y0)) → MINUS(n__0, activate(y0))
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), 0)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), 0)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), 0) at position [1] we obtained the following new rules:
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__0)) → MINUS(div(activate(y0), y1), n__0)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
IF(true, X, Y) → ACTIVATE(X)
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), 0) at position [1] we obtained the following new rules:
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__0)) → MINUS(minus(y0, y1), n__0)
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0)
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, 0) at position [1] we obtained the following new rules:
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
MINUS(n__s(y0), n__s(n__0)) → MINUS(y0, n__0)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), 0) at position [1] we obtained the following new rules:
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), n__0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(n__0)) → MINUS(s(activate(y0)), n__0)
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
IF(true, X, Y) → ACTIVATE(X)
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IF(true, X, Y) → ACTIVATE(X) we obtained the following new rules:
IF(true, n__s(n__div(n__minus(y_4, y_6), n__s(y_8))), n__0) → ACTIVATE(n__s(n__div(n__minus(y_4, y_6), n__s(y_8))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
MINUS(n__s(y0), n__s(n__s(x0))) → MINUS(y0, s(activate(x0)))
MINUS(n__s(y0), n__s(n__minus(x0, x1))) → MINUS(y0, minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(x0)) → MINUS(minus(y0, y1), x0)
MINUS(n__s(n__s(y0)), n__s(n__div(x0, x1))) → MINUS(s(activate(y0)), div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → MINUS(div(activate(y0), y1), div(activate(x0), x1))
ACTIVATE(n__div(n__s(x0), y1)) → DIV(s(activate(x0)), y1)
GEQ(n__s(n__div(y0, y1)), n__s(n__s(x0))) → GEQ(div(activate(y0), y1), s(activate(x0)))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(y0), n__s(x0)) → MINUS(y0, x0)
ACTIVATE(n__s(X)) → ACTIVATE(X)
GEQ(n__s(n__minus(y0, y1)), n__s(x0)) → GEQ(minus(y0, y1), x0)
GEQ(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → GEQ(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(x0, y1)) → DIV(x0, y1)
MINUS(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(minus(y0, y1), minus(x0, x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(minus(y0, y1), minus(x0, x1))
IF(true, n__s(n__div(n__minus(y_4, y_6), n__s(y_8))), n__0) → ACTIVATE(n__s(n__div(n__minus(y_4, y_6), n__s(y_8))))
GEQ(n__s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(n__s(x0))) → GEQ(s(activate(y0)), s(activate(x0)))
MINUS(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → MINUS(div(activate(y0), y1), minus(x0, x1))
DIV(s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → MINUS(minus(y0, y1), div(activate(x0), x1))
GEQ(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → GEQ(s(activate(y0)), minus(x0, x1))
MINUS(n__s(n__s(y0)), n__s(x0)) → MINUS(s(activate(y0)), x0)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(y0), n__s(n__minus(x0, x1))) → GEQ(y0, minus(x0, x1))
GEQ(n__s(n__s(y0)), n__s(x0)) → GEQ(s(activate(y0)), x0)
GEQ(n__s(n__s(y0)), n__s(n__div(x0, x1))) → GEQ(s(activate(y0)), div(activate(x0), x1))
GEQ(n__s(n__div(y0, y1)), n__s(n__div(x0, x1))) → GEQ(div(activate(y0), y1), div(activate(x0), x1))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(y0), n__s(n__div(x0, x1))) → MINUS(y0, div(activate(x0), x1))
MINUS(n__s(n__div(y0, y1)), n__s(n__s(x0))) → MINUS(div(activate(y0), y1), s(activate(x0)))
GEQ(n__s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(n__div(y0, y1)), n__s(x0)) → GEQ(div(activate(y0), y1), x0)
GEQ(n__s(n__div(y0, y1)), n__s(n__minus(x0, x1))) → GEQ(div(activate(y0), y1), minus(x0, x1))
MINUS(n__s(n__minus(y0, y1)), n__s(n__s(x0))) → MINUS(minus(y0, y1), s(activate(x0)))
ACTIVATE(n__div(n__minus(x0, x1), y1)) → DIV(minus(x0, x1), y1)
ACTIVATE(n__div(X1, X2)) → ACTIVATE(X1)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
MINUS(n__s(n__s(y0)), n__s(n__s(x0))) → MINUS(s(activate(y0)), s(activate(x0)))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__div(n__div(x0, x1), y1)) → DIV(div(activate(x0), x1), y1)
GEQ(n__s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__minus(X1, X2)) → MINUS(X1, X2)
MINUS(n__s(n__div(y0, y1)), n__s(x0)) → MINUS(div(activate(y0), y1), x0)
DIV(s(y0), n__s(n__div(x0, x1))) → GEQ(y0, div(activate(x0), x1))
GEQ(n__s(n__minus(y0, y1)), n__s(n__div(x0, x1))) → GEQ(minus(y0, y1), div(activate(x0), x1))
DIV(s(y0), n__s(n__s(x0))) → GEQ(y0, s(activate(x0)))
GEQ(n__s(y0), n__s(x0)) → GEQ(y0, x0)
MINUS(n__s(n__s(y0)), n__s(n__minus(x0, x1))) → MINUS(s(activate(y0)), minus(x0, x1))
The TRS R consists of the following rules:
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.